@@ -147,49 +147,36 @@ mod pindakaas {
147
147
. aggregate ( db, & lin. 0 )
148
148
. map_err ( map_unsat) ?;
149
149
match aggregated {
150
- BoolLinVariant :: Cardinality ( c) => match enc {
151
- None | Some ( Encoder :: SORTING_NETWORK ) => {
152
- SortingNetworkEncoder :: default ( ) . encode ( db, & c)
153
- }
154
- Some ( Encoder :: ADDER ) => AdderEncoder :: default ( ) . encode ( db, & c) ,
155
- Some ( Encoder :: SORTED_WEIGHT_COUNTER ) => {
156
- SwcEncoder :: default ( ) . encode ( db, & c)
157
- }
158
- Some ( Encoder :: TOTALIZER ) => TotalizerEncoder :: default ( ) . encode ( db, & c) ,
150
+ BoolLinVariant :: Cardinality ( c) => match enc. unwrap_or ( Encoder :: SORTING_NETWORK )
151
+ {
152
+ Encoder :: SORTING_NETWORK => SortingNetworkEncoder :: default ( ) . encode ( db, & c) ,
153
+ Encoder :: ADDER => AdderEncoder :: default ( ) . encode ( db, & c) ,
154
+ Encoder :: SORTED_WEIGHT_COUNTER => SwcEncoder :: default ( ) . encode ( db, & c) ,
155
+ Encoder :: TOTALIZER => TotalizerEncoder :: default ( ) . encode ( db, & c) ,
159
156
_ => return invalid_enc ( "Cardinality" , enc. unwrap ( ) ) ,
160
157
} ,
161
- BoolLinVariant :: CardinalityOne ( c) => match enc {
162
- None | Some ( Encoder :: BITWISE ) => BitwiseEncoder :: default ( ) . encode ( db, & c) ,
163
- Some ( Encoder :: ADDER ) => AdderEncoder :: default ( ) . encode ( db, & c) ,
164
- Some ( Encoder :: LADDER ) => LadderEncoder :: default ( ) . encode ( db, & c) ,
165
- Some ( Encoder :: PAIRWISE ) => PairwiseEncoder :: default ( ) . encode ( db, & c) ,
166
- Some ( Encoder :: SORTED_WEIGHT_COUNTER ) => {
167
- SwcEncoder :: default ( ) . encode ( db, & c)
168
- }
169
- Some ( Encoder :: SORTING_NETWORK ) => {
170
- SortingNetworkEncoder :: default ( ) . encode ( db, & c)
171
- }
172
- Some ( Encoder :: TOTALIZER ) => TotalizerEncoder :: default ( ) . encode ( db, & c) ,
158
+ BoolLinVariant :: CardinalityOne ( c) => match enc. unwrap_or ( Encoder :: BITWISE ) {
159
+ Encoder :: BITWISE => BitwiseEncoder :: default ( ) . encode ( db, & c) ,
160
+ Encoder :: ADDER => AdderEncoder :: default ( ) . encode ( db, & c) ,
161
+ Encoder :: LADDER => LadderEncoder :: default ( ) . encode ( db, & c) ,
162
+ Encoder :: PAIRWISE => PairwiseEncoder :: default ( ) . encode ( db, & c) ,
163
+ Encoder :: SORTED_WEIGHT_COUNTER => SwcEncoder :: default ( ) . encode ( db, & c) ,
164
+ Encoder :: SORTING_NETWORK => SortingNetworkEncoder :: default ( ) . encode ( db, & c) ,
165
+ Encoder :: TOTALIZER => TotalizerEncoder :: default ( ) . encode ( db, & c) ,
173
166
_ => return invalid_enc ( "CardinalityOne" , enc. unwrap ( ) ) ,
174
167
} ,
175
- BoolLinVariant :: Linear ( lin) => match enc {
176
- None | Some ( Encoder :: TOTALIZER ) => {
177
- TotalizerEncoder :: default ( ) . encode ( db, & lin)
178
- }
179
- Some ( Encoder :: ADDER ) => AdderEncoder :: default ( ) . encode ( db, & lin) ,
180
- Some ( Encoder :: SORTED_WEIGHT_COUNTER ) => {
181
- SwcEncoder :: default ( ) . encode ( db, & lin)
182
- }
168
+ BoolLinVariant :: Linear ( lin) => match enc. unwrap_or ( Encoder :: TOTALIZER ) {
169
+ Encoder :: TOTALIZER => TotalizerEncoder :: default ( ) . encode ( db, & lin) ,
170
+ Encoder :: ADDER => AdderEncoder :: default ( ) . encode ( db, & lin) ,
171
+ Encoder :: SORTED_WEIGHT_COUNTER => SwcEncoder :: default ( ) . encode ( db, & lin) ,
183
172
_ => return invalid_enc ( "BoolLinear" , enc. unwrap ( ) ) ,
184
173
} ,
185
174
BoolLinVariant :: Trivial => return Ok ( ( ) ) ,
186
175
}
187
176
. map_err ( map_unsat) ?;
188
177
}
189
- ConstraintArg :: Formula ( f) => match enc {
190
- None | Some ( Encoder :: TSEITIN ) => {
191
- TseitinEncoder . encode ( db, & f. 0 ) . map_err ( map_unsat) ?;
192
- }
178
+ ConstraintArg :: Formula ( f) => match enc. unwrap_or ( Encoder :: TSEITIN ) {
179
+ Encoder :: TSEITIN => TseitinEncoder . encode ( db, & f. 0 ) . map_err ( map_unsat) ?,
193
180
_ => {
194
181
return invalid_enc ( "Formula" , enc. unwrap ( ) ) ;
195
182
}
0 commit comments